Nuprl Lemma : rng_prod_wf
13,42
postcript
pdf
r
:Rng,
p
,
q
:
,
E
:({
p
..
q
}
|
r
|). (
(
r
)
p
i
<
q
.
E
(
i
))
|
r
|
latex
Up
rings
1
Definitions of Statement
Rng
,
r
xmn
,
(
r
)
i
k
<
j
.
E
(
k
)
Definitions
t
.1
,
x
.
t
(
x
)
,
|
g
|
,
r
xmn
,
x
(
s
)
,
(
r
)
i
k
<
j
.
E
(
k
)
,
t
T
,
x
:
A
.
B
(
x
)
,
Rng
Lemmas
rng
wf
,
mul
mon
of
rng
wf
,
grp
car
wf
,
int
seg
wf
,
rng
car
wf
,
mul
mon
of
rng
wf
c
,
mon
itop
wf
origin
r:Rng, p, q:
, E:({p..q
}
|r|). (
(r) p 
i < q. E(i)) 
|r| r:Rng, p, q:, E:({p..q}|r|). ((r) p i < q. E(i)) |r| 
xmn(r) i k < j. E(k)
x. t(x)xmn(r) i k < j. E(k) Tx:A. B(x)